00100	                                DRAFT
00200	
00300	            SYLLABUS FOR Ph.D. QUALIFYING EXAMINATION IN
00400	
00500	                 MATHEMATICAL THEORY OF COMPUTATION
00600	
00700	
00800		Mathematical theory of computation (MTC)  is  concerned  with
00900	the  mathematical  properties of algorithms and the computer programs
01000	that are used to express them.  It includes topics from  mathematical
01100	logic   and   recursive   function  theory,  but  in  the  qualifying
01200	examination we  shall  emphasize  those  topics  relevant  to  actual
01300	computer programs more than topics of purely mathematical interest.
01400	
01500		For  the  purposes of study, the subject may be subdivided as
01600	follows  where  the  weights  indicate  recommended  relative   study
01700	efforts though individual exams may not reflect these ratios:
01800	
01900		1. Description of algorithms (0.1).  Expression of algorithms
02000	by Turing machines [7],  Markov  algorithms  [?],  general  recursive
02100	functions  [5],  Post  canonical  systems [?], algolic programs [13],
02200	recursive  conditional  expressions  [15],  λ-expressions  [?],   and
02300	(backtrack programs (26)).
02400	
02500		2.   Computability  and  unsolvability  (0.1) [5].  Universal
02600	systems expressed as interpreters, e.g. universal Turing machines and
02700	LISP   eval  [28].    Existence  of  unsolvable  mass  problems  [5].
02800	Unsolvability of the halting problem for some form of computation and
02900	the unsolvability of the decision problem for predicate calculus [5].
03000	
03100		3.   Logic  and  set theory (0.2).  First order predicate and
03200	function calculus[1].     Interpretations  and  models  for  sets  of
03300	sentences[1].    Familiarity  with  at least one system of axioms and
03400	rules of inference and the  proof  of  the  completeness  thereof[1].
03500	Familiarity with first order axiomatizations of elementary arithmetic
03600	including an axiom schema of induction [1].  A system of  axioms  for
03700	set  theory  [1].    Second  or  omega order logic and a proof of the
03800	incompleteness of any set of axioms thereof [1].
03900	
04000		4.  Formal syntax of languages (0.2) [9].   Context free  and
04100	context  dependent  languagaes.     Regular  expressions  and  finite
04200	automata.
04300	
04400		5. Correctness and equivalence of programs (0.25).  Methods of
04500	recursion  induction [15], inductive assertions [13], and translation
04600	to first order logic [16].  Truncation induction [21].  Scott's  type
04700	theory  system  including  the  lattice  of partial functions and the
04800	properties of monotonic  and  continuous  functions  [23].   (Scott's
04900	model theory for λ-calculus (24)). (Use of Milner's proof checker LCF
05000	(22)).  Correctness including syntax [25].
05100	
05200		6.   Semantics of programming  languages  (0.15).     Abstract
05300	syntax[14].   Definition of semantics by an abstract interpreter[18].
05400	The   Vienna   definition   language[19].           Correctness    of
05500	compilers [10,(20)].
05600	
05700	Topics  and references in parentheses are included because they point
05800	to active research.  For various reasons, they will not be covered in
05900	the current examination.
06000	
06100		The ability to work problems may require some practice beyond
06200	a reading familiarity with the subject matter.  For this we recommend
06300	[7,...].
06400	
06500	
06600		The references in this draft are the  same  as  in  the  1969
06700	syllabus,  but  the  papers not actually mentioned are to be dropped,
06800	and the following are to be added:
06900	
07000	20. Painter thesis - not in exam
07100	
07200	21. Morris on truncation induction
07300	
07400	22. LCF manual by Milner.
07500	
07600	23. Scott's CUCH, ISWIM, OWHY
07700	
07800	24. Scott's model theory for λ-calculus - not in exam.
07900	
08000	25. Burstall's syntax and semantics
08100	
08200	26. Comparative schematology - Hewitt and Paterson
08300	
08400	28. McCarthy - Recursive functions of symbolic expressions and  their
08500	computation by machine. Comm. ACM 1959
08600	
08700	29. Proceedings of New Mexico Conference on proving properties of
08800	assertions.